\begin{abstract}
In the field of Software Verification, one important problem is to determine whether some code corresponds
to its specification. One way to achieve this is to (try and) prove that it cannot go wrong. This is usually done by
expressing what ``going wrong'' means as a set of boolean formulae, in terms of program variables.

\noindent	This paper presents an approach to solving such a set of constraints (\textit{ie.} trying to find an
assignment of the program variables such that all the boolean formulae do hold) over \textit{finite domains} for a
subset of the Scala language \cite{Scala}.
\end{abstract}
